Nuprl Lemma : ocmon_6
13,42
postcript
pdf
g
:OCMon,
z
:|
g
|. monot(|
g
|;
x
,
y
.
(
x
y
);
w
.
z
*
w
)
latex
Up
groups
1
Definitions
t
T
,
monot(
T
;
x
,
y
.
R
(
x
;
y
);
f
)
,
x
:
A
.
B
(
x
)
,
AntiSym(
T
;
x
,
y
.
R
(
x
;
y
))
,
Trans(
T
;
x
,
y
.
E
(
x
;
y
))
,
Refl(
T
;
x
,
y
.
E
(
x
;
y
))
,
Connex(
T
;
x
,
y
.
R
(
x
;
y
))
,
Order(
T
;
x
,
y
.
R
(
x
;
y
))
,
Cancel(
T
;
S
;
op
)
,
Linorder(
T
;
x
,
y
.
R
(
x
;
y
))
,
P
&
Q
Lemmas
ocmon
wf
,
ocmon
properties
origin
g:OCMon, z:|g|. monot(|g|;x,y.
(x 
y);
w.z * w) g:OCMon, z:|g|. monot(|g|;x,y.(x y);w.z * w) 
T